package ch.epfl.lara.matcheck.util.printer

import ch.epfl.lara.matcheck.ast._

object PrettyStringerTree extends FormatterTrees[Tree]   {
  
    override protected def format(tree: Tree): String = tree match {
      case Program(constr,extr,objs,clss) => 
        annotationformat("constraint")(constr) + NL +
          annotationformat("domain")(extr) + NL +  
        "/** classes declaration */" + NL + 
        concat(clss) + NL + 
        "/** extractor declaration */" + NL +
        concat(objs)
      
      case ObjectDef(name, invariant, methods) => 
        "object " + name + " { " + inc + NL +
          annotationformat("invariant ")(invariant) + 
          concat(methods) + dec + NL + 
        "}" + NL
      
      case FieldDef(name,tpe) => 
        "val " + name + " : " + format(tpe)
        
      case ParamDef(name,tpe) =>
        name + ": " + format(tpe)
        
      case ClassDef(isSealed,isAbs,name,fields,superc,invariant,methods) =>
        val seald = if(isSealed) "sealed " else ""
        val abstr = if(isAbs) "abstract " else ""
        val superclass = if(superc.isDefined) " extends " + superc.get else " " 
        seald + abstr + "class " + name + fields.map(format(_)).mkString("(",",",")") + superclass + " { " + inc + NL + 
          annotationformat("invariant ")(invariant) +
          concat(methods) + dec + NL + 
        "}" + NL
        
      case MethodDef(name,params,tpe,ppc,body) =>
        val annotation = ppc match {
          case None => ""  
          case Some((pre,post)) => NL +
            "/* precondition  " + PrettyStringerFormula.toString(pre) + NL +
            "   postcondition " + PrettyStringerFormula.toString(post) + NL + "*/"  
        }
              
        
        "def " + name + "(" + comma(params) + "): " + format(tpe) + " = " + 
          annotation + inc + NL + 
          format(body) + dec + NL
          
      case CaseDef(_,pattern,grd,body) => 
        "case " + format(pattern) + guard(grd) + " => " + 
          format(body) 
       
      case VarPattern(name,tpe) => name + " : " + format(tpe)
      
      case ClassPattern(name,args) => name + "(" + comma(args) + ")"
        
      case Wildcard => "_"
      
      case ObjectId(name) => name.getName
      
      case Ident(name) => name.getName
      
      case True => "true"
        
      case False => "false"
        
      case !(f) => "!("+format(f)+")"
      
      case Call(obj,method,args) => format(obj) + "." + method + "(" + comma(args) + ")"
        
      case Select(obj,field) => format(obj) + "." + field 
      
      case If(cond,then,elze) => 
        "if (" + format(cond) + ") {" + inc + NL + 
          format(then) + dec + NL + 
        "} else {" + inc + NL +
          format(elze) + dec + NL + 
        "}"
      
      case Match(selector,tpe,cases) =>
        "(" + "(" + format(selector) + ":" + format(tpe) + ")"+ " match { " + inc + NL +
          format(NL)(cases) + dec + NL +
        "}" + ")"
          
      case New(name,params) => 
        "new " + name + "(" + comma(params) + ")"
          
      case IsInstanceOf(e,tpe) =>
        format(e) + ".isInstanceOf[" + tpe + "]"
          
      case StringLit(lit) => "\"" + lit +"\""
      
      case Number(n) => n+""
        
      case +(left,right) => format(left) + " + " + format(right)
      
      case -(left,right) => format(left) + " - " + format(right)
      
      case *(left,right) => "(" + format(left) + " * " + format(right) +")"
        
      case /(left,right) => "(" + format(left) + " / " + format(right) +")"
        
      case %(left,right) => "(" + format(left) + " % " + format(right) +")"
          
      case ==(left,right) => format(left) + " == " + format(right)
      
      case <(left,right) => format(left) + " < " + format(right)
      
      case <=(left,right) => format(left) + " <= " + format(right) 
      
      case &&(left,right) => format(left) + " && " + format(right)
      
      case ||(left,right) => format(left) + " || " + format(right)
      
      case ->(left,right) => format(left) + " --> " + format(right)
      
          
      case BoolType => "Boolean"
      case IntType => "Int"
      case ClassType(name) => name
      case OptionType(seq) =>  "Option[" + (
          if (seq.length > 1) seq.map(format(_)).mkString("(",",",")")
          else format(seq.head)
                  ) + "]"
      case ParamType(tpe,ptpe) => tpe+"[" + format(ptpe) + "]"
    }
    
    private def annotationformat(prefix: String)(tree: Option[Formula]): String = tree match {
      case None => ""
      case Some(term) => "/*" + prefix + PrettyStringerFormula.toString(term) + "*/" + NL
    }
    
    
    /*
    private def format(warning: Warning): String = warning match {
      case DisjointnessFailed(cases) =>
        val message = "Checking disjointness FAILED.\n\n"
        var i = 0
        val failing = for((kase1,kase2)<-cases) yield {
          i += 1
          i+". The patterns declaration of \n\n" +
          "   " + "case " + format(kase1.pattern) + " " + guard(kase1.guard) + "\n" +
          "   " + "case " + format(kase2.pattern) + " " + guard(kase2.guard) + "\n" +
          "\n... may be overlapping."
        }
    
        failing.mkString(message,"\n\n","\n")
    
      case CompletenessFailed(incomplete) =>
        val message = "Checking completeness FAILED. Possible missing cases:\n"
        val orizontal_space = "   "
        incomplete.mkString(message+orizontal_space,"\n"+orizontal_space,"\n")
      
      case ReachabilityFailed(kase) =>
        val message = "Checking reachability FAILED.\n\n"
        message + 
        "The patterns declaration of \n\n" +
        "   case " + format(kase.pattern) + " " + guard(kase.guard) + "\n\n" +
        "... may be never reached.\n"      
          
      case ReachabilityExtractorsFailed(kase) =>
        val message = "Checking reachability FAILED.\n\n"
        message + 
        "Case \n\n" +
        "   case " + format(kase.pattern) + " " + guard(kase.guard) + "\n\n" +
        "can't be triggered because it doesn't belong to the scrutinee's type hierarchy.\n"      
          
      case NestedMatchesFailed(xs) =>
        val message = for((matchExpr,warning)<-xs ) yield {
          warning match {
            case NestedMatchesFailed(_) => format(warning)
            case _ => 
              "In nested matching expression:\n\n"+
              format(matchExpr) + "\n\n" + 
              format(warning) 
          }
        }
        
        message.mkString("\n\n")
    }
    */
}
